es:ES, e:E, l:IdLnk. es-receives(es;e;l)  E List 

latex

Definitions

Void, x:AB(x), x:AB(x), A & B, False, A, IdLnkDeq, es-eq(es), rcv-from-on(dE;dL;info;e;l;r), Type, {x:A| B(x) }, type List, S  T, receives(dE;dL;pred?;info;p;e;l), es-receives(es;e;l), EOrderAxioms(E; pred?; info), Prop, ES, es_info(es), es-pred?(es), E, pred!(e;e'), SWellFounded(R(x;y)), es-oaxioms(es), 1of(t), destination(l), loc(e), Id, s = t, e < e', P  Q, P & Q, link(e), IdLnk, P  Q, sender(e), rcv?(e), b, x:A. B(x), x:A. B(x), t  T, pred(e), first(e), a<b, , f(a)

Lemmas

rcv? wf, sender wf, nat wf, not wf, first wf, pred wf, IdLnk wf, event system wf, es-oaxioms wf, EOrderAxioms wf, es-pred!-wellfounded, receives wf, es-pred? wf, assert wf, rcv-from-on wf, es-E wf, Id wf, es-eq wf, idlnk-deq wf, es info wf